/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BAXB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRK30/FONT#10=ZERO30/FONT#11=BAXI30/FONT#12=MS25



␈↓ ↓H␈↓α␈↓ ↓aEXPANDING THE ROLE OF VERIFICATION IN COMPUTER SCIENCE EDUCATION

␈↓ ↓H␈↓␈↓ α_The␈αfact␈αthat␈αcomputer␈αprograms␈αare␈αstill␈αdebugged␈αis␈αa␈αcontinuing␈αdisgrace␈αto␈αanyone␈αwho
␈↓ ↓H␈↓thinks␈αmathematically.␈α The␈αway␈αof␈αgetting␈αa␈αprogram␈αcorrect␈αshould␈αbe␈αto␈αprove␈αthat␈αit␈αmeets␈αits
␈↓ ↓H␈↓specifications␈α
and␈α∞check␈α
this␈α∞proof␈α
with␈α
a␈α∞computer.␈α
 As␈α∞much␈α
as␈α
possible,␈α∞the␈α
proof␈α∞should␈α
be
␈↓ ↓H␈↓computer generated.

␈↓ ↓H␈↓␈↓ α_Of␈α
course,␈α
this␈α
has␈αbeen␈α
the␈α
goal␈α
of␈α
program␈αverification␈α
research␈α
for␈α
many␈α
years,␈αand␈α
good
␈↓ ↓H␈↓progress␈α
has␈αbeen␈α
made.␈α In␈α
fact␈αthe␈α
progress␈α
has␈αbeen␈α
good␈αenough␈α
so␈αthat␈α
now␈αcomputer␈α
science
␈↓ ↓H␈↓education lags behind the science.  Correcting this lag requires the following at Stanford:

␈↓ ↓H␈↓␈↓ α_1.␈α∂Verification␈α∂should␈α∂be␈α∂separated␈α∂from␈α∂complexity␈α∂theory,␈α∂automata␈α∂theory␈α∂and␈α∞formal
␈↓ ↓H␈↓language␈α↔theory␈α⊗as␈α↔qualifying␈α↔exam␈α⊗area␈α↔and␈α⊗as␈α↔a␈α↔section␈α⊗of␈α↔the␈α↔comprehensive␈α⊗exam.
␈↓ ↓H␈↓Verification␈α≡should␈α≥include␈α≡Hoare-type␈α≥methods,␈α≡verification␈α≥condition␈α≡generation,␈α≥the
␈↓ ↓H␈↓Cartwright-McCarthy␈αmethod␈α
of␈αexpressing␈α
LISP␈αprograms␈αas␈α
first␈αorder␈α
sentences,␈αand␈αthe␈α
Scott
␈↓ ↓H␈↓formalisms.  A first step is the preparation of a qualifying exam syllabus.

␈↓ ↓H␈↓␈↓ α_2.␈α⊂A␈α∂subset␈α⊂of␈α⊂this␈α∂should␈α⊂be␈α⊂on␈α∂the␈α⊂comprehensive␈α⊂syllabus.␈α∂ This␈α⊂should␈α⊂include␈α∂and
␈↓ ↓H␈↓might␈α
be␈α
limited␈α
to␈α
the␈α
material␈α
on␈α
invariants␈α
in␈α
Manna's␈α
book␈α
and␈α
the␈α
material␈α
on␈α
first␈α
order
␈↓ ↓H␈↓representation␈αin␈αthe␈αMcCarthy␈αand␈αTalcott␈αbook.␈α The␈αnecessary␈αbackground␈αin␈αfirst␈αorder␈αlogic
␈↓ ↓H␈↓might be included in this part of the syllabus, especially since it is in the Manna book.

␈↓ ↓H␈↓␈↓ α_3.␈α
The␈α∞programming␈α
problem␈α∞on␈α
the␈α
Comprehensive␈α∞should␈α
require␈α∞that␈α
the␈α∞program␈α
be
␈↓ ↓H␈↓verified.␈α Given␈αthe␈αpresent␈αstate␈αof␈α
verification,␈αthis␈αwould␈αprobably␈αrequire␈αmaking␈αit␈α
somewhat
␈↓ ↓H␈↓less␈α
ambitious␈α
as␈αa␈α
programming␈α
problem,␈αbut␈α
this␈α
part␈αof␈α
the␈α
exam␈αhas␈α
already␈α
received␈αmuch
␈↓ ↓H␈↓criticism␈αas␈α
not␈αa␈α
scientific␈αexercise.␈α This␈α
cannot␈αbe␈α
done␈αuntil␈αthe␈α
one␈αor␈α
another␈αof␈αthe␈α
machine
␈↓ ↓H␈↓verification systems has been made available for general use.

␈↓ ↓H␈↓␈↓ α_4.␈α
The␈α
LISP␈α
course,␈α
now␈α
206,␈α
and␈α
soon␈α
to␈α
be␈α
126,␈α
should␈α
require␈α
machine␈α
verification␈αof
␈↓ ↓H␈↓some␈α∞of␈α∞its␈α
programs,␈α∞perhaps␈α∞all␈α∞pure␈α
LISP␈α∞programs.␈α∞ This␈α
requires␈α∞the␈α∞implementation␈α∞of␈α
a
␈↓ ↓H␈↓predicate␈αcalculus␈α
proof-checker␈αas␈αa␈α
feature␈αof␈αthe␈α
student␈αMaclisp␈αsystem.␈α
 Making␈αsuch␈αa␈α
systee
␈↓ ↓H␈↓will be a major task, and we should get NSF to support a project aimed at this goal.

␈↓ ↓H␈↓␈↓ α_5.␈α∃CS105␈α∃and␈α∃106␈α∃should␈α∃contain␈α∃some␈α∃verification.␈α∃ The␈α∃goal␈α∃of␈α⊗a␈α∃machine-aided
␈↓ ↓H␈↓verification␈αsystem␈α
for␈αthese␈α
courses␈αis␈α
vaguer␈αin␈αmy␈α
mind,␈αand␈α
therefore␈αapparently␈α
further␈αoff.
␈↓ ↓H␈↓However,␈α⊂perhaps␈α⊂the␈α⊂PASCAL␈α⊂enthusiast␈α⊃would␈α⊂think␈α⊂otherwise␈α⊂and␈α⊂would␈α⊂be␈α⊃prepared␈α⊂to
␈↓ ↓H␈↓undertake␈α∞to␈α∞produce␈α∞a␈α∞PASCAL␈α∞verification␈α∞system␈α∞that␈α∞could␈α∞be␈α∞used␈α∞in␈α∂elementary␈α∞courses.
␈↓ ↓H␈↓Most likely this would also be a project that would require outside support.

␈↓ ↓H␈↓␈↓ α_6.␈αIt␈αis␈αpossible␈αthat␈αlarge␈αamounts␈αof␈αstudent␈αverification␈αwill␈αincrease␈αour␈αcomputer␈αpower
␈↓ ↓H␈↓requirements.

␈↓ ↓H␈↓␈↓ α_Stanford␈α
has␈α∞strong␈α
enough␈α∞faculty␈α
interests␈α∞in␈α
verification␈α∞including␈α
Floyd␈α∞(not␈α
presently
␈↓ ↓H␈↓active␈α⊂here),␈α⊂Luckham,␈α⊂Manna,␈α⊂McCarthy,␈α⊂and␈α⊂Owicki,␈α⊃so␈α⊂that␈α⊂we␈α⊂are␈α⊂in␈α⊂a␈α⊂good␈α⊃position␈α⊂to
␈↓ ↓H␈↓initiate the effort.  Weyhrauch, Talcott and Karp strengthen this effort.

␈↓ ↓H␈↓␈↓ α_A␈α∞large␈α∞project␈α∂supported␈α∞by␈α∞the␈α∞education␈α∂part␈α∞of␈α∞NSF␈α∞aimed␈α∂at␈α∞making␈α∞it␈α∂practical␈α∞to
␈↓ ↓H␈↓include verification in programming courses might be a good form of organization.